;;;===========================================================================
;;;
;;; The compositions of two reductions is a reduction
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 03/05/10 || End date: 03/05/10
;;;
;;;===========================================================================


(in-package "ACL2")

(include-book "algebraic-data-structures")

(encapsulate
 
 ;;**************************************************
 ;; Signaturas
 ;;**************************************************

 (
 ;;--------------------------------------------------
 ;; The signatures of the ring-cmps R
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-ring-cmps *) => *)
 ;; Addition operation ring-cmps
 ((addition-ring-cmps * *)=> *)
 ;; Product operation ring-cmps
 ((product-ring-cmps * *) => *)
 ;; Inverse-Cmpsring-cmps
 ((inverse-cmps *) => *)
 ;; Zero element ring-cmps
 ((zero-element-cmps) => *)
 ;; Unit element ring-cmps
 ((unit-cmps )=> *)

 ;;--------------------------------------------------
 ;; Top Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-top * *) => *)
 ;; Group Operation 
 ((group-operation-top * * *) => *)
 ;; Zero element
 ((zero-top *) => *)
 ;; External multiplication
 ((external-top * * *) => *)
 ;; Inverse-Cmpselement
 ((inverse-top * *) => *)

 ;;--------------------------------------------------
 ;; The top differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-top * *) => *)

 ;;--------------------------------------------------
 ;; Middle Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-middle * *) => *)
 ;; Group Operation 
 ((group-operation-middle * * *) => *)
 ;; Zero element
 ((zero-middle *) => *)
 ;; External multiplication
 ((external-middle * * *) => *)
 ;; Inverse-Cmpselement
 ((inverse-middle * *) => *)

 ;;--------------------------------------------------
 ;; The middle differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-middle * *) => *)


 ;;--------------------------------------------------
 ;; Bottom Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-bottom * *) => *)
 ;; Group Operation 
 ((group-operation-bottom * * *) => *)
 ;; Zero element
 ((zero-bottom *) => *)
 ;; External multiplication
 ((external-bottom * * *) => *)
 ;; Inverse element
 ((inverse-bottom * *) => *)

 ;;--------------------------------------------------
 ;; The bottom differential
 ;;--------------------------------------------------

 ;; The differential
 ((d-bottom * *) => *)


 ;;--------------------------------------------------
 ;; The f top morphism
 ;;--------------------------------------------------

 ;; The function
 ((f2 * *) => *)

 ;;--------------------------------------------------
 ;; The g top morphism
 ;;--------------------------------------------------

 ;; The function
 ((g2 * *) => *)


 ;;--------------------------------------------------
 ;; The h top morphism
 ;;--------------------------------------------------

 ;; The function
 ((h2 * *) => *)


 ;;--------------------------------------------------
 ;; The f bottom morphism
 ;;--------------------------------------------------

 ;; The function
 ((f1 * *) => *)

 ;;--------------------------------------------------
 ;; The g bottom morphism
 ;;--------------------------------------------------

 ;; The function
 ((g1 * *) => *)


 ;;--------------------------------------------------
 ;; The h bottom morphism
 ;;--------------------------------------------------

 ;; The function
 ((h1 * *) => *)



 
 )
 ;;**************************************************
 ;; Witnesses
 ;;**************************************************
 
 ;;--------------------------------------------------
 ;; The witnesses of the ring-cmps Z
 ;;--------------------------------------------------

 ;; The characteristic function

 (local (defun inv-ring-cmps (a)
	  (integerp a)))
 
 ;; Addition operation Z
 (local (defun addition-ring-cmps (a b)
	  (+ a b)))

 ;; Product operation ring-cmps
 (local (defun product-ring-cmps (a b)
	  (* a b)))

 ;; Inverse addition
 (local (defun inverse-cmps(a)
	  (- a)))

 ;; Zero element ring-cmps
 (local (defun zero-element-cmps nil
	  0))

 ;; Unit element ring-cmps
 (local (defun unit-cmps nil
	  1))

 ;;--------------------------------------------------
 ;; Top Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-top (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-top (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-top (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-top (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-top (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The top differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-top (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; Middle Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-middle (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-middle (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-middle (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-middle (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-middle (n a)
	  (declare (ignore n a))
	  0))

 ;;--------------------------------------------------
 ;; The middle differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-middle (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; Bottom Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-bottom (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-bottom (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-bottom (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-bottom (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse bottom
 (local (defun inverse-bottom (n a)
	  (declare (ignore n a))
	  0))

 


 ;;--------------------------------------------------
 ;; The bottom differential
 ;;--------------------------------------------------
 
  ;; The differential
 (local (defun d-bottom (n a)
	  (declare (ignore n a))
	  0))

 
 

 ;;--------------------------------------------------
 ;; The f top morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun f2 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The g top morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun g2 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The h top morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun h2 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The f bottom morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun f1 (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The g bottom morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun g1 (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; The h bottom morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun h1 (n a)
	  (declare (ignore n a))
	  0))

 


  ;;************************************************** 
  ;; Properties
  ;;************************************************** 

(check-reduction-p
(reduction 
 (chain-complex 
   'inv-ring-cmps 'addition-ring-cmps 'zero-element-cmps 'inverse-cmps 'product-ring-cmps 'unit-cmps
   'inv-top 'group-operation-top 'zero-top 'external-top 'inverse-top 'd-top
   )
 (chain-complex 
   'inv-ring-cmps 'addition-ring-cmps 'zero-element-cmps 'inverse-cmps 'product-ring-cmps 'unit-cmps 
   'inv-middle 'group-operation-middle 'zero-middle 'external-middle 'inverse-middle 'd-middle )
   'f2  'g2  'h2
   ) 'reduction2)


(check-reduction-p
(reduction 
 (chain-complex 
   'inv-ring-cmps 'addition-ring-cmps 'zero-element-cmps 'inverse-cmps 'product-ring-cmps 'unit-cmps 
   'inv-middle 'group-operation-middle 'zero-middle 'external-middle 'inverse-middle 'd-middle )
  (chain-complex 
    'inv-ring-cmps 'addition-ring-cmps 'zero-element-cmps 'inverse-cmps 'product-ring-cmps 'unit-cmps 
    'inv-bottom 'group-operation-bottom 'zero-bottom 'external-bottom 'inverse-bottom 'd-bottom )
  'f1  'g1  'h1 
   ) 'reduction1)


)


;;==================================================
;; The new definitions
;;==================================================


 ;;--------------------------------------------------
 ;; New Top Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
(defun new-inv-top (n a) 
   (inv-top n a))

 ;; Group Operation 
(defun new-group-operation-top (n a b)
	  (group-operation-top n a b))

 ;; Zero element
(defun new-zero-top (n)
   (zero-top n))

 ;; External multiplication
(defun new-external-top (n a b)
	 (external-top n a b))

 ;; Inverse element
(defun new-inverse-top (n a)
   (inverse-top n a))
	 


 ;;--------------------------------------------------
 ;; The new top differential 
 ;;--------------------------------------------------

 ;; The differential
(defun new-d-top (n a)
  (d-top n a))


 ;;--------------------------------------------------
 ;; New Bottom Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
(defun new-inv-bottom (n a) 
   (inv-bottom n a))
	  

 ;; Group Operation 
(defun new-group-operation-bottom (n a b)
	  (group-operation-bottom n a b))
	  

 ;; Zero element
(defun new-zero-bottom (n)
  (zero-bottom n))
	  

 ;; External multiplication
(defun new-external-bottom (n a b)
   (external-bottom n a b))


 ;; Inverse bottom
(defun new-inverse-bottom (n a)
  (inverse-bottom n a))
 


 ;;--------------------------------------------------
 ;; The new bottom differential
 ;;--------------------------------------------------
 
  ;; The differential
(defun new-d-bottom (n a)
   (d-bottom n a))
	  

 ;;--------------------------------------------------
 ;; The new f morphism
 ;;--------------------------------------------------

 ;; The function
(defun new-f (n a)
   (f1 n (f2 n a)))
	  


 ;;--------------------------------------------------
 ;; The new g morphism
 ;;--------------------------------------------------

 ;; The function
(defun new-g (n a)
   (g2 n (g1 n a)))
	  

 

 ;;--------------------------------------------------
 ;; The new h morphism
 ;;--------------------------------------------------

 ;; The function
(defun new-h (n a)
   (group-operation-top (1+ n) (h2 n a) (g2 (1+ n) (h1 n (f2 n a)))))
	  


;;===========================================================================
;; The properties
;;===========================================================================

(encapsulate 
 
 ()


(defthm closure-d-bottom
   (implies (and (inv-bottom n a) (integerp n))
	    (inv-bottom (+ n -1) (d-bottom n a)))
  :hints (("Goal" :use ((:instance |REDUCTION1-is-a-reduction|)))))

(defthm closure-d-bottom-2
   (implies (and (inv-bottom n a) (integerp n))
	    (inv-bottom (+ -1 n) (d-bottom n a)))
  :hints (("Goal" :use ((:instance closure-d-bottom)))))


(defthm closure-d-top
   (implies (and (inv-top n a) (integerp n))
	    (inv-top (+ n -1) (d-top n a)))
  :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|)))))

(defthm closure-d-top-2
   (implies (and (inv-top n a) (integerp n))
	    (inv-top (+ -1 n) (d-top n a)))
  :hints (("Goal" :use ((:instance closure-d-top)))))

(defthm commutativity-group-operation-bottom 
  (implies (and (inv-bottom n a)
		(inv-bottom n b)
		(integerp n))
	   (equal (group-operation-bottom n a b)
		  (group-operation-bottom n b a))))

(defthm bottom-aux-prop1
  (implies (and (inv-bottom n a)
		(inv-bottom n b)
		(inv-bottom n c)
		(integerp n))
	   (equal (group-operation-bottom n (group-operation-bottom n a b) c)
		  (group-operation-bottom n a (group-operation-bottom n b c))))
  :hints (("Goal" :use ((:instance |REDUCTION1-is-a-reduction|)))))

(defthm bottom-aux-prop2
  (implies (and (inv-bottom n a)
		(inv-bottom n b)
		(inv-bottom n c)
		(integerp n))
	   (equal (group-operation-bottom n c (group-operation-bottom n a b))
		  (group-operation-bottom n a (group-operation-bottom n b c))))
  :hints (("Goal" :use ((:instance bottom-aux-prop1)
			(:instance commutativity-group-operation-bottom 
				   (a (group-operation-bottom n a b))
				   (b c))))))


(defthm commutativity-group-operation-top
  (implies (and (inv-top n a)
		(inv-top n b)
		(integerp n))
	   (equal (group-operation-top n a b)
		  (group-operation-top n b a))))


(defthm top-aux-prop1
  (implies (and (inv-top n a)
		(inv-top n b)
		(inv-top n c)
		(integerp n))
	   (equal (group-operation-top n (group-operation-top n a b) c)
		  (group-operation-top n a (group-operation-top n b c))))
  :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|)))))


(defthm top-aux-prop2
  (implies (and (inv-top n a)
		(inv-top n b)
		(inv-top n c)
		(integerp n))
	   (equal (group-operation-top n c (group-operation-top n a b))
		  (group-operation-top n a (group-operation-top n b c))))
  :hints (("Goal" :use ((:instance top-aux-prop1)
			(:instance commutativity-group-operation-top 
				   (a (group-operation-top n a b))
				   (b c))))))


(defthm new-closure-f
   (implies (and (new-inv-top n a) (integerp n))
	    (new-inv-bottom n (new-f n a))))

 (defthm new-closure-g
   (implies (and (new-inv-bottom n a) (integerp n))
	    (new-inv-top n (new-g n a))))

 (defthm closure-h2
   (implies (and (inv-top n a) (integerp n))
	    (inv-top (+ n 1) (h2 n a)))
   :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|)))))

(defthm closure-h2-2
   (implies (and (inv-top n a) (integerp n))
	    (inv-top (+ 1 n) (h2 n a)))
   :hints (("Goal" :use ((:instance closure-h2)))))


(defthm closure-f2
  (implies (and (inv-top n a) (integerp n))
	   (inv-middle n (f2 n a)))
  :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|)))))

(defthm closure-h1
  (implies (and (inv-middle n a) (integerp n))
	   (inv-middle (+ n 1) (h1 n a)))
  :hints (("Goal" :use ((:instance |REDUCTION1-is-a-reduction|)))))


(defthm closure-g2
  (implies (and (inv-middle n a) (integerp n))
	   (inv-top n (g2 n a)))
  :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|)))))

(defthm closure-g2-2
  (implies (and (inv-middle (+ n 1) a) (integerp n))
	   (inv-top (+ n 1) (g2 (+ n 1) a)))
  :hints (("Goal" :use ((:instance  closure-g2 (n (+ n 1)))))))



(defthm closure-g2-h1-f2
  (implies (and (inv-top n a) (integerp n))
	   (inv-top (+ n 1) (g2 (+ n 1) (h1 n (f2 n a)))))
  :hints (("Goal" :use ((:instance closure-f2)
			(:instance closure-h1 (a (f2 n a)))
			(:instance closure-g2-2 (a (h1 n (f2 n a))))))))

(defthm closure-g2-h1-f2-2
  (implies (and (inv-top n a) (integerp n))
	   (inv-top (+ 1 n) (g2 (+ 1 n) (h1 n (f2 n a)))))
  :hints (("Goal" :use ((:instance closure-g2-h1-f2)))))



(local (defthm external-top-g2
  (implies (and (inv-middle n a)
		(inv-ring-cmps r)
		(integerp n))
	   (equal (external-top n r (g2 n a))
		  (g2 n (external-middle n r a))))
  :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|)))))
)


(defthm external-top-g2-2
  (implies (and (inv-middle (+ 1 n) a)
		(inv-ring-cmps r)
		(integerp n))
	   (equal (external-top (+ 1 n) r (g2 (+ 1 n) a))
		  (g2 (+ 1 n) (external-middle (+ 1 n) r a))))
  :hints (("Goal" :use ((:instance external-top-g2 ( n (+ 1 n)))))))

(defthm external-top-g2-3
  (implies (and (inv-top n a)
		(inv-ring-cmps r)
		(integerp n))
	   (equal (external-top (+ 1 n) r (g2 (+ 1 n) (h1 n (f2 n a))))
		  (g2 (+ 1 n) (external-middle (+ 1 n) r (h1 n (f2 n a))))))
  :hints (("Goal" :use ((:instance closure-f2)
			(:instance closure-h1 (a (f2 n a)))
			(:instance external-top-g2-2 (a (h1 n (f2 n a))))))))


)



(encapsulate
 ()


(local (defthm 1-1+n
   (implies (integerp n)
	    (equal (+ 1 -1 n) n))))

(local (defthm 1-1+n2
   (implies (integerp n)
	    (equal (+ -1 1 n) n))))



 (defthm associativity-operation-abelian-group-tcc
   (implies (and (inv-top n a)
		 (inv-top n b)
		 (inv-top n c)
		 (integerp n))
	    (equal (group-operation-top n (group-operation-top n a b) c)
		   (group-operation-top n a (group-operation-top n b c))))
   :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|)))))


(local (defthm commutativity-associativity-group-operation-top
  (implies (and (inv-top n a)
		(inv-top n b)
		(inv-top n c)
		(inv-top n d)
		(integerp n))
	   (equal (group-operation-top n
				(group-operation-top n a b)
				(group-operation-top n c d))
	   (group-operation-top n (group-operation-top n a c)
				(group-operation-top n b d))))
  :hints (("Goal" :use ((:instance associativity-operation-abelian-group-tcc
				   (c (group-operation-top n c d)))
			(:instance associativity-operation-abelian-group-tcc
				   (a b) (b c) (c d))
			(:instance commutativity-group-operation-top
				   (a b) (b c))
			(:instance associativity-operation-abelian-group-tcc
				   (a c) (b b) (c d))
			(:instance associativity-operation-abelian-group-tcc
				   (a a) (b c) (c (group-operation-top n b d)))))))
)

(local (defthm inv-h2-d-top2
  (implies (and (integerp n) (inv-top n a))
	   (inv-top (1+ (1- n)) (h2 (1- n) (d-top n a))))
  :hints (("Goal" :in-theory (disable 1-1+n)))))

(local (defthm inv-h2-d-top
  (implies (and (integerp n) (inv-top n a))
	   (inv-top n (h2 (1- n) (d-top n a))))
  :hints (("Goal" :use ((:instance inv-h2-d-top2))))))


(local (defthm inv-h1-f2-d-middle2
  (implies (and (integerp n) (inv-top n a))
	   (inv-middle (1+ (1- n)) (h1 (1- n) (f2 (1- n) (d-top n a)))))
  :hints (("Goal"
	   :use ((:instance closure-f2 (a (d-top n a)) (n (1- n)))
		 (:instance closure-h1 (a (f2 (1- n) (d-top n a))) (n (1- n))))))))

(local (defthm inv-h1-f2-d-middle
  (implies (and (integerp n) (inv-top n a))
	   (inv-middle n (h1 (1- n) (f2 (1- n) (d-top n a)))))
  :hints (("Goal"  :use ((:instance inv-h1-f2-d-middle2))))))


(local (defthm inv-g2-h1-f2-d-top
  (implies (and (integerp n) (inv-top n a))
	   (inv-top n (g2 n (h1 (1- n) (f2 (1- n) (d-top n a))))))))
 
  
(local (defthm inv-d-top-h2-2
  (implies (and (integerp n) (inv-top n a))
	   (inv-top (1- (1+ n)) (d-top (1+ n) (h2 n a))))
  :hints (("Goal"
	   :use ((:instance closure-d-top (n (1+ n))
			    (a (h2 n a))))))))

(local (defthm inv-d-top-h2
  (implies (and (integerp n) (inv-top n a))
	   (inv-top n (d-top (1+ n) (h2 n a))))
  :hints (("Goal" :use ((:instance inv-d-top-h2-2))))))

(local (defthm inv-middle-h1-f2
  (implies (and (inv-top n a) (integerp n))
	   (inv-middle (1+ n) (h1 n (f2 n a))))
  :hints (("Goal"
	   :use ((:instance closure-f2)
		 (:instance closure-h1 (a (f2 n a)))))))
)

(local (defthm
    closure-d-middle
    (implies (and (inv-middle n a) (integerp n))
             (inv-middle (+ n -1) (d-middle n a)))
  :hints
  (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|))))))

(local (defthm inv-d-middle-h1-f2-2
  (implies (and (integerp n) (inv-top n a))
	   (inv-middle (1- (1+ n)) (d-middle (1+ n) (h1 n (f2 n a)))))
   :hints (("Goal" :use ((:instance inv-middle-h1-f2)
			 (:instance closure-d-middle (n (1+ n))
				    (a (h1 n (f2 n a)))))))))

(local (defthm inv-d-middle-h1-f2
  (implies (and (integerp n) (inv-top n a))
	   (inv-middle n (d-middle (1+ n) (h1 n (f2 n a)))))
  :hints (("Goal"  :use ((:instance inv-d-middle-h1-f2-2))))))


(local (defthm inv-g2-d-middle-h1-f2
  (implies (and (integerp n) (inv-top n a))
	   (inv-top n (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))))


(local (defthm new-hod+doh-aux-1
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top 
		   n (group-operation-top n (h2 (1- n) (d-top n a))
					  (g2 n (h1 (1- n) (f2 (1- n) (d-top n a)))))
		   (group-operation-top n (d-top (1+ n) (h2 n a))
					  (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))
		  (group-operation-top 
		   n (group-operation-top n (h2 (1- n) (d-top n a))
					  (d-top (1+ n) (h2 n a)))
		   (group-operation-top n (g2 n (h1 (1- n) (f2 (1- n) (d-top n a)))) 
					  (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))
		  ))))

(local (defthm h2-d-d-h2
	 (implies (and (inv-top n a) (integerp n))
		  (equal (group-operation-top n (h2 (+ -1 n) (d-top n a))
					  (d-top (+ 1 n) (h2 n a)))
			 (group-operation-top n a (inverse-top n (g2 n (f2 n a))))))
	 :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction| (gnrt a)))))
		  ))


(local (defthm new-hod+doh-aux-2
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top 
		   n (group-operation-top n (h2 (1- n) (d-top n a))
					  (g2 n (h1 (1- n) (f2 (1- n) (d-top n a)))))
		   (group-operation-top n (d-top (1+ n) (h2 n a))
					  (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))
		  (group-operation-top 
		   n (group-operation-top n a (inverse-top n (g2 n (f2 n a))))
		   (group-operation-top n (g2 n (h1 (1- n) (f2 (1- n) (d-top n a)))) 
					  (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))
		  ))
  :hints (("Goal" :use ((:instance new-hod+doh-aux-1)
			(:instance h2-d-d-h2))))))



(local (defthm new-hod+doh-aux-3
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top 
		   n (group-operation-top n (h2 (1- n) (d-top n a))
					  (g2 n (h1 (1- n) (f2 (1- n) (d-top n a)))))
		   (group-operation-top n (d-top (1+ n) (h2 n a))
					  (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))
		  (group-operation-top 
		   n (group-operation-top n a  (inverse-top n (g2 n (f2 n a))))
		   (g2 n (group-operation-middle n (h1 (1- n) (f2 (1- n) (d-top n a)))
					     (d-middle (1+ n) (h1 n (f2 n a)))))
		  )))
  :hints (("Goal" :use ((:instance new-hod+doh-aux-2)
			)))))

(local (defthm new-hod+doh-aux-4
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top 
		   n (group-operation-top n (h2 (1- n) (d-top n a))
					  (g2 n (h1 (1- n) (f2 (1- n) (d-top n a)))))
		   (group-operation-top n (d-top (1+ n) (h2 n a))
					  (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))
		  (group-operation-top 
		   n (group-operation-top n a  (inverse-top n (g2 n (f2 n a))))
		   (g2 n (group-operation-middle n (h1 (1- n) (d-middle n (f2 n a)))
					     (d-middle (1+ n) (h1 n (f2 n a)))))
		  )))
  :hints (("Goal" :use ((:instance new-hod+doh-aux-3)
			)))))

(local  (defthm h1od+doh1
   (implies (and (inv-middle n gnrt) (integerp n))
	    (equal (group-operation-middle n (h1 (+ -1 n) (d-middle n gnrt))
		      (d-middle (+ 1 n) (h1 n gnrt)))
		   (group-operation-middle n gnrt
		      (inverse-middle n (g1 n (f1 n gnrt))))))
   :hints (("Goal" :use ((:instance |REDUCTION1-is-a-reduction|))))))

(local  (defthm h1od+doh1-2
   (implies (and (inv-middle n gnrt) (integerp n))
	    (equal (group-operation-middle n (h1 (1- n) (d-middle n gnrt))
		      (d-middle (1+ n) (h1 n gnrt)))
		   (group-operation-middle n gnrt
		      (inverse-middle n (g1 n (f1 n gnrt))))))
   :hints (("Goal" :use ((:instance h1od+doh1))))))


(local (defthm new-hod+doh-aux-5
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top 
		   n (group-operation-top n (h2 (1- n) (d-top n a))
					  (g2 n (h1 (1- n) (f2 (1- n) (d-top n a)))))
		   (group-operation-top n (d-top (1+ n) (h2 n a))
					  (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))
		  (group-operation-top 
		   n (group-operation-top n a  (inverse-top n (g2 n (f2 n a))))
		   (g2 n (group-operation-middle n (f2 n a) (inverse-middle n (g1 n (f1 n (f2 n a)))))
		  ))))
  :hints (("Goal" :use ((:instance h1od+doh1-2 (gnrt (f2 n a)))
			(:instance new-hod+doh-aux-4))))))

(local (defthm new-hod+doh-aux-6
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top 
		   n (group-operation-top n (h2 (1- n) (d-top n a))
					  (g2 n (h1 (1- n) (f2 (1- n) (d-top n a)))))
		   (group-operation-top n (d-top (1+ n) (h2 n a))
					  (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))
		  (group-operation-top 
		   n (group-operation-top n a  (inverse-top n (g2 n (f2 n a))))
		   (group-operation-top n (g2 n (f2 n a))
					   (g2 n (inverse-middle n (g1 n (f1 n (f2 n a)))))
		  ))))
  :hints (("Goal" :use ((:instance new-hod+doh-aux-5))))))




(local (defthm g2-inverse-middle-inverse-top-g2-aux1
  (implies (and (inv-middle n a) (integerp n))
	   (equal (g2 n (group-operation-middle n a (inverse-middle n a)))
		  (group-operation-top n (g2 n a) (g2 n (inverse-middle n a)))))
  :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction| (b (inverse-middle n a)))) ))))

(local (defthm g2-inverse-middle-inverse-top-g2-aux2
  (implies (and (inv-middle n a) (integerp n))
	   (equal (g2 n (group-operation-middle n a (inverse-middle n a)))
		  (zero-top n)))
  ))


(local (defthm g2-inverse-middle-inverse-top-g2-aux3
  (implies (and (inv-middle n a) (integerp n))
	   (equal (group-operation-top n (g2 n a) (g2 n (inverse-middle n a)))
		  (zero-top n)))
  :hints (("Goal" :use ((:instance g2-inverse-middle-inverse-top-g2-aux1)
			(:instance g2-inverse-middle-inverse-top-g2-aux2)))))
)

(local (defthm closure-g2-inverse
  (implies (and (inv-middle n a) (integerp n))
	   (inv-top n (g2 n (inverse-middle n a))))))

(local (defthm g2-inverse-middle-inverse-top-g2
  (implies (and (inv-middle n a) (integerp n))
	   (equal (inverse-top n (g2 n a))
		  (g2 n (inverse-middle n a))
		  )))
  )
  


(local (defthm new-hod+doh-aux-7
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top 
		   n (group-operation-top n (h2 (1- n) (d-top n a))
					  (g2 n (h1 (1- n) (f2 (1- n) (d-top n a)))))
		   (group-operation-top n (d-top (1+ n) (h2 n a))
					  (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))
		  (group-operation-top 
		   n (group-operation-top n a  (inverse-top n (g2 n (f2 n a))))
		   (group-operation-top n (g2 n (f2 n a))
					(inverse-top n (g2 n (g1 n (f1 n (f2 n a)))))
					    ))))
  :hints (("Goal" :in-theory (disable |REDUCTION2-is-a-reduction|)
:use ((:instance g2-inverse-middle-inverse-top-g2)
			(:instance new-hod+doh-aux-6))))))


(local  (defthm existence-inverse-element-tcc
   (implies (and (inv-top n a) (integerp n))
	    (equal (group-operation-top n a (inverse-top n a))
		   (zero-top n)))
   :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|))))))

(local (defthm group-operation-inverse-deletion
  (implies (and (inv-top n a)
		(inv-top n b)
		(inv-top n c)
		(integerp n))
	   (equal (group-operation-top n (group-operation-top n a (inverse-top n b))
				       (group-operation-top n b c))
		  (group-operation-top n a c)))
  :hints (("Goal" :use ((:instance associativity-operation-abelian-group-tcc
				   (b (inverse-top n b))
				   (c (group-operation-top n b c)))
			(:instance associativity-operation-abelian-group-tcc
				   (a (inverse-top n b)))
			(:instance commutativity-group-operation-top
				   (a (inverse-top n b)))
			(:instance existence-inverse-element-tcc
				   (a b))
			(:instance commutativity-group-operation-top
				   (a (zero-top n)) (b c))
			(:instance existence-inverse-element-tcc
				   (a c)))))))

(local (defthm closure-g2-f2
	 (implies (and (inv-top n a) (integerp n))
		  (inv-top n (g2 n (f2 n a))))))


(local (defthm closure-g2-g1-f1-f2
	 (implies (and (inv-top n a) (integerp n))
		  (inv-top n (g2 n (g1 n (f1 n (f2 n a))))))))




(local (defthm new-hod+doh-aux
  (implies (and (inv-top n a) (integerp n))
	   (equal (group-operation-top 
		   n (group-operation-top n (h2 (1- n) (d-top n a))
					  (g2 n (h1 (1- n) (f2 (1- n) (d-top n a)))))
		   (group-operation-top n (d-top (1+ n) (h2 n a))
					  (g2 n (d-middle (1+ n) (h1 n (f2 n a))))))
		  (group-operation-top n a
				       (inverse-top n (g2 n (g1 n (f1 n (f2 n a))))))))
  :hints (("Goal" :in-theory (disable |REDUCTION2-is-a-reduction|)
	   :use ((:instance closure-g2-f2)
			(:instance closure-g2-g1-f1-f2)
			(:instance new-hod+doh-aux-7)
			(:instance group-operation-inverse-deletion
				   (b (g2 n (f2 n a)))
				   (c (inverse-top n (g2 n (g1 n (f1 n (f2 n a)))))))))))
	)	   


(defthm new-hod+doh
    (implies (and (new-inv-top n a) (integerp n))
	     (equal (new-group-operation-top n (new-h (1- n) (new-d-top n a))
		       (new-d-top (1+ n) (new-h n a)))
		    (new-group-operation-top n
		     a (new-inverse-top n (new-g n (new-f n a)))))
	     )
    :hints (("Goal" :in-theory (disable G2-INVERSE-MIDDLE-INVERSE-TOP-G2)
	     :use ((:instance new-hod+doh-aux)))))

(defthm new-hod+doh-bis
    (implies (and (inv-top n a) (integerp n))
	     (equal (group-operation-top n (new-h (+ -1 n) (d-top n a))
		       (d-top (+ 1 n) (new-h n a)))
		    (group-operation-top n
		     a (inverse-top n (new-g n (new-f n a)))))
	     )
    :hints (("Goal"
	     :use ((:instance new-hod+doh)))))

)


(encapsulate
 ()


 (local (defthm f2-g2
	  (implies (and (inv-middle n gnrt) (integerp n))
		   (equal (f2 n (g2 n gnrt))
			  gnrt))
	  :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|))))
	  ))


 (local (defthm f1-h1
	  (implies (and (inv-middle n gnrt) (integerp n))
		   (equal (f1 (+ 1 n) (h1 n gnrt))
			  (zero-bottom (+ 1 n))))
	  :hints (("Goal" :use ((:instance |REDUCTION1-is-a-reduction|))))
	  ))

(defthm f1-f2-g2-h1
	 (implies (and (inv-top n gnrt) (integerp n))
		  (equal (f1 (+ 1 n) (f2 (+ 1 n) (g2 (+ 1 n) (h1 n (f2 n gnrt)))))
			 (zero-bottom (+ 1 n))))
	 :hints (("Goal" :use ((:instance closure-f2)
			       (:instance closure-h1 (a (f2 n gnrt)))
			       (:instance f2-g2 (gnrt (h1 n (f2 n gnrt)))
					  (n (+ 1 n)))
			       (:instance f1-h1 (gnrt (f2 n gnrt))
					  )))))
)



(encapsulate
 ()

 (local (DEFTHM CLOSURE-H1-bis
                      (IMPLIES (and (INV-MIDDLE N A) (integerp n))
                               (INV-MIDDLE (1+ N) (H1 N A)))
		      :hints (("Goal" :use ((:instance CLOSURE-H1))))))

 (local (DEFTHM CLOSURE-H2-bis
                      (IMPLIES (and (INV-top N A) (integerp n))
                               (INV-top (1+ N) (H2 N A)))
		      :hints (("Goal" :use ((:instance CLOSURE-H2))))))

 (local (DEFTHM CLOSURE-ZERO-ELEMENT-MCC
                      (INV-MIDDLE N (ZERO-MIDDLE N))))

 (local (DEFTHM CLOSURE-ZERO-ELEMENT-TCC
                      (INV-TOP N (ZERO-TOP N))))

 (local (DEFTHM COMMUTATIVITY-TCC
                      (IMPLIES (AND (INV-TOP N A) (INV-TOP N B) (integerp n))
                               (EQUAL (GROUP-OPERATION-TOP N A B)
                                      (GROUP-OPERATION-TOP N B A)))))
 
 (local (DEFTHM DISTRIBUTIVITY-F2
                      (IMPLIES (AND (INV-TOP N A) (INV-TOP N B) (integerp n))
                               (EQUAL (F2 N (GROUP-OPERATION-TOP N A B))
                                      (GROUP-OPERATION-MIDDLE N (F2 N A)
                                                              (F2 N B))))))
 (local (DEFTHM DISTRIBUTIVITY-G2
                      (IMPLIES (AND (INV-MIDDLE N A) (INV-MIDDLE N B) (integerp n))
                               (EQUAL (G2 N (GROUP-OPERATION-MIDDLE N A B))
                                      (GROUP-OPERATION-TOP N (G2 N A)
                                                           (G2 N B))))))

 (local (DEFTHM DISTRIBUTIVITY-H1
                      (IMPLIES (AND (INV-MIDDLE N A) (INV-MIDDLE N B) (integerp n))
                               (EQUAL (H1 N (GROUP-OPERATION-MIDDLE N A B))
                                      (GROUP-OPERATION-MIDDLE (1+ N)
                                                              (H1 N A)
                                                              (H1 N B))))))
 (local (DEFTHM DISTRIBUTIVITY-H2
                      (IMPLIES (AND (INV-TOP N A) (INV-TOP N B) (integerp n))
                               (EQUAL (H2 N (GROUP-OPERATION-TOP N A B))
                                      (GROUP-OPERATION-TOP (1+ N)
                                                           (H2 N A)
                                                           (H2 N B))))))

 (local (DEFTHM
                 EXISTENCE-IDENTITY-ELEMENT-MCC
                 (IMPLIES (and (INV-MIDDLE N A) (integerp n))
                          (EQUAL (GROUP-OPERATION-MIDDLE N A (ZERO-MIDDLE N))
                                 A))))

 (local (DEFTHM EXISTENCE-IDENTITY-ELEMENT-TCC
                      (IMPLIES (and (INV-TOP N A) (integerp n))
                               (EQUAL (GROUP-OPERATION-TOP N A (ZERO-TOP N))
                                      A))))


 (local (DEFTHM F2OG2
                      (IMPLIES (and (INV-MIDDLE N GNRT) (integerp n))
                               (EQUAL (F2 N (G2 N GNRT)) GNRT))))

 (local (DEFTHM F2OH2
                      (IMPLIES (and (INV-TOP N GNRT) (integerp n))
                               (EQUAL (F2 (1+ N) (H2 N GNRT))
                                      (ZERO-MIDDLE (1+ N))))))

 (local (DEFTHM G2-0
	  (implies (integerp n)
		   (EQUAL (G2 N (ZERO-MIDDLE N))
			  (ZERO-TOP N)))))
 
 (local (DEFTHM H1-0
	  (implies (integerp n)
                      (EQUAL (H1 N (ZERO-MIDDLE N))
                             (ZERO-MIDDLE (1+ N))))))

 (local (DEFTHM H1OH1
                      (IMPLIES (and (INV-MIDDLE N GNRT) (integerp n))
                               (EQUAL (H1 (1+ N) (H1 N GNRT))
                                      (ZERO-MIDDLE (1+ (1+ N)))))))

 (local (DEFTHM H2OG2
                      (IMPLIES (and (INV-MIDDLE N GNRT) (integerp n))
                               (EQUAL (H2 N (G2 N GNRT))
                                      (ZERO-TOP (1+ N))))))
 (local (DEFTHM H2OH2
                      (IMPLIES (and (INV-TOP N GNRT) (integerp n))
                               (EQUAL (H2 (1+ N) (H2 N GNRT))
                                      (ZERO-TOP (1+ (1+ N)))))))

 (defthm subgoal1-aux
   (IMPLIES (and (new-INV-TOP N GNRT) (integerp n))
	    (EQUAL (NEW-H (+ 1 N) (NEW-H N GNRT))
                (new-ZERO-TOP (1+ (+ 1 N)))))
	 :hints (("Goal" :in-theory (disable |REDUCTION1-is-a-reduction|
					     |REDUCTION2-is-a-reduction|)
		 )))

 (defthm subgoal1
   (IMPLIES (and (INV-TOP N GNRT) (integerp n))
	    (EQUAL (NEW-H (+ 1 N) (NEW-H N GNRT))
                (ZERO-TOP (+ 1 1 N))))
	 :hints (("Goal" :use ((:instance subgoal1-aux))
		 )))


 (local (defthm associativity-commutativity-operation-abelian-group-tcc2
   (implies (and (inv-top n a)
		 (inv-top n b)
		 (inv-top n c)
		 (integerp n))
	    (equal (group-operation-top n a (group-operation-top n b c) )
		   (group-operation-top n b (group-operation-top n a c))))
   :hints (("Goal" :use ((:instance associativity-operation-abelian-group-tcc)
			 (:instance commutativity-group-operation-top)
			 (:instance associativity-operation-abelian-group-tcc (a b) (b a))))))
	)

 (local (DEFTHM CLOSURE-OPERATION-ABELIAN-GROUP-TCC
                      (IMPLIES (AND (INV-TOP N A) (INV-TOP N B) (integerp n))
                               (INV-TOP N (GROUP-OPERATION-TOP N A B)))))

 (defthm new-distributivity-h
   (implies (and (new-inv-top n a)
		 (new-inv-top n b)
		 (integerp n))
	    (equal (new-h n (new-group-operation-top n a b))
		   (new-group-operation-top (1+ n) (new-h n a) (new-h n b))))
	    :hints (("Goal" :in-theory (disable  CLOSURE-G2-H1-F2-2
						|REDUCTION1-is-a-reduction|
						|REDUCTION2-is-a-reduction|)
		 )))

)


(encapsulate

 ()
(local (DEFTHM CLOSURE-H1-bis
                      (IMPLIES (and (INV-MIDDLE N A) (integerp n))
                               (INV-MIDDLE (1+ N) (H1 N A)))
		      :hints (("Goal" :use ((:instance CLOSURE-H1))))))


 (local (defthm g2-inverse
   (implies (and (inv-middle (+ 1 n) a) (integerp n))
	    (equal (g2 (+ 1 n) (inverse-middle (+ 1 n) a))
		   (inverse-top (+ 1 n) (g2 (+ 1 n) a))))))

 (defthm g2-inverse-2
   (implies (and (inv-top n a) (integerp n))
	    (equal (g2 (+ 1 n) (inverse-middle (+ 1 n) (h1 n (f2 n a))))
		   (inverse-top (+ 1 n) (g2 (+ 1 n) (h1 n (f2 n a))))))
   :hints (("Goal" :use ((:instance closure-f2)
			 (:instance CLOSURE-H1-bis)
			 (:instance g2-inverse 
		    (a (h1 n (f2 n a))))))))

 )


(defthm group-operation-zero-top
  (implies (and (inv-top n gnrt)
		(integerp n))
	   (equal (group-operation-top n
				       (zero-top n)
				       gnrt)
		  gnrt)))

(defthm group-operation-zero-middle
  (implies (and (inv-middle n gnrt)
		(integerp n))
	   (equal (group-operation-middle n
				       (zero-middle n)
				       gnrt)
		  gnrt)))




(defthm f2-g2
	  (implies (and (inv-middle n gnrt) (integerp n))
		   (equal (f2 n (g2 n gnrt))
			  gnrt))
	  :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|))))
	  )

(defthm h1-h1
	  (implies (and (inv-middle n gnrt) (integerp n))
		   (equal (h1 (+ 1 n) (h1 n gnrt))
			  (zero-middle (+ 1 1 n))))
	  :hints (("Goal" :use ((:instance |REDUCTION1-is-a-reduction|))))
	  )


(defthm h2-g2
  (implies (and (inv-middle n  gnrt) (integerp n))
	   (equal (h2 n (g2 n gnrt))
		  (zero-top (+ 1 n))))
  :hints (("Goal" :use ((:instance |REDUCTION2-is-a-reduction|))))
	  )

(defthm h2-g2-bis
  (implies (and (inv-middle (+ 1 n) gnrt) (integerp n))
	   (equal (h2 (+ 1 n) (g2 (+ 1 n) gnrt))
		  (zero-top (+ 1 (+ 1 n)))))
  :hints (("Goal" :use ((:instance h2-g2 (n (+ 1 n))))))
	  )



(defthm g2-h1-f2-g2-h1-f2
  (implies (and (inv-top n gnrt)
		(integerp n))
	   (equal (G2 (+ 1 1 N)
		      (H1 (+ 1 N)
			  (F2 (+ 1 N)
			      (G2 (+ 1 N) (H1 N (F2 N GNRT))))))
		  (ZERO-TOP (+ 1 1 N))))
  :hints (("Goal" :USE ((:INSTANCE CLOSURE-F2)
                                  (:INSTANCE CLOSURE-H1 (A (F2 N GNRT)))
                                  (:INSTANCE F2-G2 (GNRT (H1 N (F2 N GNRT)))
                                             (N (+ 1 N)))
                                  (:INSTANCE h1-H1 (GNRT (F2 N GNRT)))))))
	   


(defthm h2-g2-h1-f2
  (implies (and (inv-top n gnrt)
		(integerp n))
	   (EQUAL (H2 (+ 1 N)
                    (G2 (+ 1 N) (H1 N (F2 N GNRT))))
                (ZERO-TOP (+ 1 1 N))))
  :hints (("Goal" :USE ((:INSTANCE CLOSURE-F2)
                                  (:INSTANCE CLOSURE-H1 (A (F2 N GNRT)))
                                  (:INSTANCE H2-G2 (GNRT (H1 N (F2 N GNRT)))
                                             (N (+ 1 N)))
                                  ))))

(check-reduction-p
(reduction 
   (chain-complex 
    'inv-ring-cmps 'addition-ring-cmps 'zero-element-cmps 'inverse-cmps 'product-ring-cmps 'unit-cmps
    'new-inv-top 'new-group-operation-top 'new-zero-top 'new-external-top 'new-inverse-top 'new-d-top )
    (chain-complex 
     'inv-ring-cmps 'addition-ring-cmps 'zero-element-cmps 'inverse-cmps 'product-ring-cmps 'unit-cmps
     'new-inv-bottom 'new-group-operation-bottom 'new-zero-bottom 'new-external-bottom 'new-inverse-bottom 'new-d-bottom )
   'new-f  'new-g 'new-h) 
   'cmps-reduction1-reduction2
   :hints '(("Subgoal 51" :use ((:instance top-aux-prop2)))
	   ("Subgoal 35" :use ((:instance bottom-aux-prop2)))
	   ("Subgoal 15" :use ((:instance new-distributivity-h)))
	   ("Subgoal 4" :use ((:instance new-hod+doh (a gnrt))))))

;;;===========================================================================
;;;
;;; End of the proof of the compositions of reductions
;;;
;;;===========================================================================


;;;----------------------------------------------------------------------------
;;; 
;;; Defining the generic theory:
;;;
;;;----------------------------------------------------------------------------


(include-book "generic-theory")


#|
(get-event-lst 
 '(perturbation
   new-inv-top
   new-group-operation-top
   new-zero-top
   new-external-top 
   new-inverse-top
   new-d-top
   new-inv-bottom 
   new-group-operation-bottom
   new-zero-bottom 
   new-external-bottom
   new-inverse-bottom
   new-d-bottom
   new-f
   new-g 
   new-h 
   |CMPS-REDUCTION1-REDUCTION2-is-a-reduction|
   )
 )
|#


(defconst *cmps*
  '((ENTER-BOOT-STRAP-MODE :MSWINDOWS)
 (DEFUN NEW-INV-TOP (N A) (INV-TOP N A))
 (DEFUN NEW-GROUP-OPERATION-TOP (N A B)
        (GROUP-OPERATION-TOP N A B))
 (DEFUN NEW-ZERO-TOP (N) (ZERO-TOP N))
 (DEFUN NEW-EXTERNAL-TOP (N A B)
        (EXTERNAL-TOP N A B))
 (DEFUN NEW-INVERSE-TOP (N A)
        (INVERSE-TOP N A))
 (DEFUN NEW-D-TOP (N A) (D-TOP N A))
 (DEFUN NEW-INV-BOTTOM (N A)
        (INV-BOTTOM N A))
 (DEFUN NEW-GROUP-OPERATION-BOTTOM (N A B)
        (GROUP-OPERATION-BOTTOM N A B))
 (DEFUN NEW-ZERO-BOTTOM (N)
        (ZERO-BOTTOM N))
 (DEFUN NEW-EXTERNAL-BOTTOM (N A B)
        (EXTERNAL-BOTTOM N A B))
 (DEFUN NEW-INVERSE-BOTTOM (N A)
        (INVERSE-BOTTOM N A))
 (DEFUN NEW-D-BOTTOM (N A)
        (D-BOTTOM N A))
 (DEFUN NEW-F (N A) (F1 N (F2 N A)))
 (DEFUN NEW-G (N A) (G2 N (G1 N A)))
 (DEFUN NEW-H (N A)
        (GROUP-OPERATION-TOP (1+ N)
                             (H2 N A)
                             (G2 (1+ N) (H1 N (F2 N A)))))
 (DEFTHM
  |CMPS-REDUCTION1-REDUCTION2-is-a-reduction|
  (AND
   (AND
    (AND
     (AND
      (AND
       (AND
           (AND (AND (IMPLIES (AND (INV-RING-CMPS X) (INV-RING-CMPS Y))
                              (INV-RING-CMPS (ADDITION-RING-CMPS X Y)))
                     (IMPLIES (AND (INV-RING-CMPS X)
                                   (INV-RING-CMPS Y)
                                   (INV-RING-CMPS Z))
                              (EQUAL (ADDITION-RING-CMPS (ADDITION-RING-CMPS X Y) Z)
                                     (ADDITION-RING-CMPS X (ADDITION-RING-CMPS Y Z)))))
                (IMPLIES (INV-RING-CMPS X)
                         (EQUAL (ADDITION-RING-CMPS (ZERO-ELEMENT-CMPS) X)
                                X))
                (IMPLIES (INV-RING-CMPS X)
                         (EQUAL (ADDITION-RING-CMPS X (ZERO-ELEMENT-CMPS))
                                X))
                (INV-RING-CMPS (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (EQUAL (ADDITION-RING-CMPS (INVERSE-CMPS X) X)
                           (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (EQUAL (ADDITION-RING-CMPS X (INVERSE-CMPS X))
                           (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (INV-RING-CMPS (INVERSE-CMPS X))))
       (AND (AND (IMPLIES (AND (INV-RING-CMPS X) (INV-RING-CMPS Y))
                          (INV-RING-CMPS (PRODUCT-RING-CMPS X Y)))
                 (IMPLIES (AND (INV-RING-CMPS X)
                               (INV-RING-CMPS Y)
                               (INV-RING-CMPS Z))
                          (EQUAL (PRODUCT-RING-CMPS (PRODUCT-RING-CMPS X Y) Z)
                                 (PRODUCT-RING-CMPS X (PRODUCT-RING-CMPS Y Z)))))
            (IMPLIES (INV-RING-CMPS X)
                     (EQUAL (PRODUCT-RING-CMPS (UNIT-CMPS) X) X))
            (IMPLIES (INV-RING-CMPS X)
                     (EQUAL (PRODUCT-RING-CMPS X (UNIT-CMPS)) X))
            (INV-RING-CMPS (UNIT-CMPS)))
       (IMPLIES (AND (INV-RING-CMPS X)
                     (INV-RING-CMPS Y)
                     (INV-RING-CMPS Z))
                (EQUAL (PRODUCT-RING-CMPS X (ADDITION-RING-CMPS Y Z))
                       (ADDITION-RING-CMPS (PRODUCT-RING-CMPS X Y)
                                      (PRODUCT-RING-CMPS X Z))))
       (IMPLIES (AND (INV-RING-CMPS X)
                     (INV-RING-CMPS Y)
                     (INV-RING-CMPS Z))
                (EQUAL (PRODUCT-RING-CMPS (ADDITION-RING-CMPS X Y) Z)
                       (ADDITION-RING-CMPS (PRODUCT-RING-CMPS X Z)
                                      (PRODUCT-RING-CMPS Y Z)))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (NEW-INV-TOP N (NEW-GROUP-OPERATION-TOP N A B)))
      (IMPLIES
       (AND (NEW-INV-TOP N A)
            (NEW-INV-TOP N B)
            (NEW-INV-TOP N C)
            (INTEGERP N))
       (EQUAL (NEW-GROUP-OPERATION-TOP N (NEW-GROUP-OPERATION-TOP N A B)
                                       C)
              (NEW-GROUP-OPERATION-TOP N A (NEW-GROUP-OPERATION-TOP N B C))))
      (NEW-INV-TOP N (NEW-ZERO-TOP N))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (NEW-INV-TOP N (NEW-EXTERNAL-TOP N R A)))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A (NEW-ZERO-TOP N))
                      A))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (NEW-INV-TOP N (NEW-INVERSE-TOP N A)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N)
                    (EQUAL (NEW-GROUP-OPERATION-TOP N A B)
                           (NEW-ZERO-TOP N)))
               (EQUAL (NEW-INVERSE-TOP N A) B))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A (NEW-INVERSE-TOP N A))
                      (NEW-ZERO-TOP N)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A B)
                      (NEW-GROUP-OPERATION-TOP N B A)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N R (NEW-GROUP-OPERATION-TOP N A B))
                      (NEW-GROUP-OPERATION-TOP N (NEW-EXTERNAL-TOP N R A)
                                               (NEW-EXTERNAL-TOP N R B))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING-CMPS S)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (ADDITION-RING-CMPS S R)
                                        A)
                      (NEW-GROUP-OPERATION-TOP N (NEW-EXTERNAL-TOP N S A)
                                               (NEW-EXTERNAL-TOP N R A))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING-CMPS S)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (PRODUCT-RING-CMPS S R)
                                        A)
                      (NEW-EXTERNAL-TOP N S (NEW-EXTERNAL-TOP N R A))))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (UNIT-CMPS) A) A))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-TOP N (NEW-GROUP-OPERATION-TOP N A B))
                      (NEW-GROUP-OPERATION-TOP N (NEW-INVERSE-TOP N A)
                                               (NEW-INVERSE-TOP N B))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING-CMPS S)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-TOP N (NEW-EXTERNAL-TOP N S A))
                      (NEW-EXTERNAL-TOP N S (NEW-INVERSE-TOP N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (NEW-INVERSE-TOP N (NEW-ZERO-TOP N))
                      (NEW-ZERO-TOP N)))
      (IMPLIES (AND (INV-RING-CMPS S) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N S (NEW-ZERO-TOP N))
                      (NEW-ZERO-TOP N))))
     (AND (AND (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                        (NEW-INV-TOP (+ N -1) (NEW-D-TOP N A)))
               (IMPLIES (AND (NEW-INV-TOP N A)
                             (NEW-INV-TOP N B)
                             (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-GROUP-OPERATION-TOP N A B))
                               (NEW-GROUP-OPERATION-TOP (+ N -1)
                                                        (NEW-D-TOP N A)
                                                        (NEW-D-TOP N B))))
               (IMPLIES (AND (NEW-INV-TOP N A)
                             (INV-RING-CMPS R)
                             (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-EXTERNAL-TOP N R A))
                               (NEW-EXTERNAL-TOP (+ N -1)
                                                 R (NEW-D-TOP N A))))
               (IMPLIES (INTEGERP N)
                        (EQUAL (NEW-D-TOP N (NEW-ZERO-TOP N))
                               (NEW-ZERO-TOP (+ N -1))))
               (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-INVERSE-TOP N A))
                               (NEW-INVERSE-TOP (+ N -1)
                                                (NEW-D-TOP N A)))))
          (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                   (EQUAL (NEW-D-TOP (1- N) (NEW-D-TOP N A))
                          (NEW-ZERO-TOP (1- (1- N)))))))
    (AND
     (AND
      (AND
       (AND
           (AND (AND (IMPLIES (AND (INV-RING-CMPS X) (INV-RING-CMPS Y))
                              (INV-RING-CMPS (ADDITION-RING-CMPS X Y)))
                     (IMPLIES (AND (INV-RING-CMPS X)
                                   (INV-RING-CMPS Y)
                                   (INV-RING-CMPS Z))
                              (EQUAL (ADDITION-RING-CMPS (ADDITION-RING-CMPS X Y) Z)
                                     (ADDITION-RING-CMPS X (ADDITION-RING-CMPS Y Z)))))
                (IMPLIES (INV-RING-CMPS X)
                         (EQUAL (ADDITION-RING-CMPS (ZERO-ELEMENT-CMPS) X)
                                X))
                (IMPLIES (INV-RING-CMPS X)
                         (EQUAL (ADDITION-RING-CMPS X (ZERO-ELEMENT-CMPS))
                                X))
                (INV-RING-CMPS (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (EQUAL (ADDITION-RING-CMPS (INVERSE-CMPS X) X)
                           (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (EQUAL (ADDITION-RING-CMPS X (INVERSE-CMPS X))
                           (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (INV-RING-CMPS (INVERSE-CMPS X))))
       (AND (AND (IMPLIES (AND (INV-RING-CMPS X) (INV-RING-CMPS Y))
                          (INV-RING-CMPS (PRODUCT-RING-CMPS X Y)))
                 (IMPLIES (AND (INV-RING-CMPS X)
                               (INV-RING-CMPS Y)
                               (INV-RING-CMPS Z))
                          (EQUAL (PRODUCT-RING-CMPS (PRODUCT-RING-CMPS X Y) Z)
                                 (PRODUCT-RING-CMPS X (PRODUCT-RING-CMPS Y Z)))))
            (IMPLIES (INV-RING-CMPS X)
                     (EQUAL (PRODUCT-RING-CMPS (UNIT-CMPS) X) X))
            (IMPLIES (INV-RING-CMPS X)
                     (EQUAL (PRODUCT-RING-CMPS X (UNIT-CMPS)) X))
            (INV-RING-CMPS (UNIT-CMPS)))
       (IMPLIES (AND (INV-RING-CMPS X)
                     (INV-RING-CMPS Y)
                     (INV-RING-CMPS Z))
                (EQUAL (PRODUCT-RING-CMPS X (ADDITION-RING-CMPS Y Z))
                       (ADDITION-RING-CMPS (PRODUCT-RING-CMPS X Y)
                                      (PRODUCT-RING-CMPS X Z))))
       (IMPLIES (AND (INV-RING-CMPS X)
                     (INV-RING-CMPS Y)
                     (INV-RING-CMPS Z))
                (EQUAL (PRODUCT-RING-CMPS (ADDITION-RING-CMPS X Y) Z)
                       (ADDITION-RING-CMPS (PRODUCT-RING-CMPS X Z)
                                      (PRODUCT-RING-CMPS Y Z)))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B)))
      (IMPLIES
       (AND (NEW-INV-BOTTOM N A)
            (NEW-INV-BOTTOM N B)
            (NEW-INV-BOTTOM N C)
            (INTEGERP N))
       (EQUAL
          (NEW-GROUP-OPERATION-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B)
                                      C)
          (NEW-GROUP-OPERATION-BOTTOM N
                                      A (NEW-GROUP-OPERATION-BOTTOM N B C))))
      (NEW-INV-BOTTOM N (NEW-ZERO-BOTTOM N))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A (NEW-ZERO-BOTTOM N))
                      A))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-INVERSE-BOTTOM N A)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N)
                    (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A B)
                           (NEW-ZERO-BOTTOM N)))
               (EQUAL (NEW-INVERSE-BOTTOM N A) B))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
           (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A (NEW-INVERSE-BOTTOM N A))
                  (NEW-ZERO-BOTTOM N)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A B)
                      (NEW-GROUP-OPERATION-BOTTOM N B A)))
      (IMPLIES
          (AND (NEW-INV-BOTTOM N A)
               (NEW-INV-BOTTOM N B)
               (INV-RING-CMPS R)
               (INTEGERP N))
          (EQUAL (NEW-EXTERNAL-BOTTOM N R (NEW-GROUP-OPERATION-BOTTOM N A B))
                 (NEW-GROUP-OPERATION-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A)
                                             (NEW-EXTERNAL-BOTTOM N R B))))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A)
                (INV-RING-CMPS S)
                (INV-RING-CMPS R)
                (INTEGERP N))
           (EQUAL (NEW-EXTERNAL-BOTTOM N (ADDITION-RING-CMPS S R)
                                       A)
                  (NEW-GROUP-OPERATION-BOTTOM N (NEW-EXTERNAL-BOTTOM N S A)
                                              (NEW-EXTERNAL-BOTTOM N R A))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING-CMPS S)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N (PRODUCT-RING-CMPS S R)
                                           A)
                      (NEW-EXTERNAL-BOTTOM N S (NEW-EXTERNAL-BOTTOM N R A))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N (UNIT-CMPS) A)
                      A))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A)
                (NEW-INV-BOTTOM N B)
                (INTEGERP N))
           (EQUAL (NEW-INVERSE-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B))
                  (NEW-GROUP-OPERATION-BOTTOM N (NEW-INVERSE-BOTTOM N A)
                                              (NEW-INVERSE-BOTTOM N B))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING-CMPS S)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-BOTTOM N (NEW-EXTERNAL-BOTTOM N S A))
                      (NEW-EXTERNAL-BOTTOM N S (NEW-INVERSE-BOTTOM N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (NEW-INVERSE-BOTTOM N (NEW-ZERO-BOTTOM N))
                      (NEW-ZERO-BOTTOM N)))
      (IMPLIES (AND (INV-RING-CMPS S) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N S (NEW-ZERO-BOTTOM N))
                      (NEW-ZERO-BOTTOM N))))
     (AND
      (AND
          (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                   (NEW-INV-BOTTOM (+ N -1)
                                   (NEW-D-BOTTOM N A)))
          (IMPLIES (AND (NEW-INV-BOTTOM N A)
                        (NEW-INV-BOTTOM N B)
                        (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B))
                          (NEW-GROUP-OPERATION-BOTTOM (+ N -1)
                                                      (NEW-D-BOTTOM N A)
                                                      (NEW-D-BOTTOM N B))))
          (IMPLIES (AND (NEW-INV-BOTTOM N A)
                        (INV-RING-CMPS R)
                        (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A))
                          (NEW-EXTERNAL-BOTTOM (+ N -1)
                                               R (NEW-D-BOTTOM N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (NEW-D-BOTTOM N (NEW-ZERO-BOTTOM N))
                          (NEW-ZERO-BOTTOM (+ N -1))))
          (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-INVERSE-BOTTOM N A))
                          (NEW-INVERSE-BOTTOM (+ N -1)
                                              (NEW-D-BOTTOM N A)))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-D-BOTTOM (1- N) (NEW-D-BOTTOM N A))
                      (NEW-ZERO-BOTTOM (1- (1- N)))))))
    (AND (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                  (NEW-INV-BOTTOM N (NEW-F N A)))
         (IMPLIES (AND (NEW-INV-TOP N A)
                       (NEW-INV-TOP N B)
                       (INTEGERP N))
                  (EQUAL (NEW-F N (NEW-GROUP-OPERATION-TOP N A B))
                         (NEW-GROUP-OPERATION-BOTTOM N (NEW-F N A)
                                                     (NEW-F N B))))
         (IMPLIES (AND (NEW-INV-TOP N A)
                       (INV-RING-CMPS R)
                       (INTEGERP N))
                  (EQUAL (NEW-F N (NEW-EXTERNAL-TOP N R A))
                         (NEW-EXTERNAL-BOTTOM N R (NEW-F N A))))
         (IMPLIES (INTEGERP N)
                  (EQUAL (NEW-F N (NEW-ZERO-TOP N))
                         (NEW-ZERO-BOTTOM N)))
         (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                  (EQUAL (NEW-F N (NEW-INVERSE-TOP N A))
                         (NEW-INVERSE-BOTTOM N (NEW-F N A)))))
    (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
             (EQUAL (NEW-D-BOTTOM N (NEW-F N A))
                    (NEW-F (1- N) (NEW-D-TOP N A)))))
   (AND (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                 (NEW-INV-TOP (+ N 1) (NEW-H N A)))
        (IMPLIES (AND (NEW-INV-TOP N A)
                      (NEW-INV-TOP N B)
                      (INTEGERP N))
                 (EQUAL (NEW-H N (NEW-GROUP-OPERATION-TOP N A B))
                        (NEW-GROUP-OPERATION-TOP (+ N 1)
                                                 (NEW-H N A)
                                                 (NEW-H N B))))
        (IMPLIES (AND (NEW-INV-TOP N A)
                      (INV-RING-CMPS R)
                      (INTEGERP N))
                 (EQUAL (NEW-H N (NEW-EXTERNAL-TOP N R A))
                        (NEW-EXTERNAL-TOP (+ N 1)
                                          R (NEW-H N A))))
        (IMPLIES (INTEGERP N)
                 (EQUAL (NEW-H N (NEW-ZERO-TOP N))
                        (NEW-ZERO-TOP (+ N 1))))
        (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                 (EQUAL (NEW-H N (NEW-INVERSE-TOP N A))
                        (NEW-INVERSE-TOP (+ N 1) (NEW-H N A)))))
   (AND
    (AND
     (AND
      (AND
       (AND
           (AND (AND (IMPLIES (AND (INV-RING-CMPS X) (INV-RING-CMPS Y))
                              (INV-RING-CMPS (ADDITION-RING-CMPS X Y)))
                     (IMPLIES (AND (INV-RING-CMPS X)
                                   (INV-RING-CMPS Y)
                                   (INV-RING-CMPS Z))
                              (EQUAL (ADDITION-RING-CMPS (ADDITION-RING-CMPS X Y) Z)
                                     (ADDITION-RING-CMPS X (ADDITION-RING-CMPS Y Z)))))
                (IMPLIES (INV-RING-CMPS X)
                         (EQUAL (ADDITION-RING-CMPS (ZERO-ELEMENT-CMPS) X)
                                X))
                (IMPLIES (INV-RING-CMPS X)
                         (EQUAL (ADDITION-RING-CMPS X (ZERO-ELEMENT-CMPS))
                                X))
                (INV-RING-CMPS (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (EQUAL (ADDITION-RING-CMPS (INVERSE-CMPS X) X)
                           (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (EQUAL (ADDITION-RING-CMPS X (INVERSE-CMPS X))
                           (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (INV-RING-CMPS (INVERSE-CMPS X))))
       (AND (AND (IMPLIES (AND (INV-RING-CMPS X) (INV-RING-CMPS Y))
                          (INV-RING-CMPS (PRODUCT-RING-CMPS X Y)))
                 (IMPLIES (AND (INV-RING-CMPS X)
                               (INV-RING-CMPS Y)
                               (INV-RING-CMPS Z))
                          (EQUAL (PRODUCT-RING-CMPS (PRODUCT-RING-CMPS X Y) Z)
                                 (PRODUCT-RING-CMPS X (PRODUCT-RING-CMPS Y Z)))))
            (IMPLIES (INV-RING-CMPS X)
                     (EQUAL (PRODUCT-RING-CMPS (UNIT-CMPS) X) X))
            (IMPLIES (INV-RING-CMPS X)
                     (EQUAL (PRODUCT-RING-CMPS X (UNIT-CMPS)) X))
            (INV-RING-CMPS (UNIT-CMPS)))
       (IMPLIES (AND (INV-RING-CMPS X)
                     (INV-RING-CMPS Y)
                     (INV-RING-CMPS Z))
                (EQUAL (PRODUCT-RING-CMPS X (ADDITION-RING-CMPS Y Z))
                       (ADDITION-RING-CMPS (PRODUCT-RING-CMPS X Y)
                                      (PRODUCT-RING-CMPS X Z))))
       (IMPLIES (AND (INV-RING-CMPS X)
                     (INV-RING-CMPS Y)
                     (INV-RING-CMPS Z))
                (EQUAL (PRODUCT-RING-CMPS (ADDITION-RING-CMPS X Y) Z)
                       (ADDITION-RING-CMPS (PRODUCT-RING-CMPS X Z)
                                      (PRODUCT-RING-CMPS Y Z)))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B)))
      (IMPLIES
       (AND (NEW-INV-BOTTOM N A)
            (NEW-INV-BOTTOM N B)
            (NEW-INV-BOTTOM N C)
            (INTEGERP N))
       (EQUAL
          (NEW-GROUP-OPERATION-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B)
                                      C)
          (NEW-GROUP-OPERATION-BOTTOM N
                                      A (NEW-GROUP-OPERATION-BOTTOM N B C))))
      (NEW-INV-BOTTOM N (NEW-ZERO-BOTTOM N))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A (NEW-ZERO-BOTTOM N))
                      A))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (NEW-INV-BOTTOM N (NEW-INVERSE-BOTTOM N A)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N)
                    (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A B)
                           (NEW-ZERO-BOTTOM N)))
               (EQUAL (NEW-INVERSE-BOTTOM N A) B))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
           (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A (NEW-INVERSE-BOTTOM N A))
                  (NEW-ZERO-BOTTOM N)))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (NEW-INV-BOTTOM N B)
                    (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-BOTTOM N A B)
                      (NEW-GROUP-OPERATION-BOTTOM N B A)))
      (IMPLIES
          (AND (NEW-INV-BOTTOM N A)
               (NEW-INV-BOTTOM N B)
               (INV-RING-CMPS R)
               (INTEGERP N))
          (EQUAL (NEW-EXTERNAL-BOTTOM N R (NEW-GROUP-OPERATION-BOTTOM N A B))
                 (NEW-GROUP-OPERATION-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A)
                                             (NEW-EXTERNAL-BOTTOM N R B))))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A)
                (INV-RING-CMPS S)
                (INV-RING-CMPS R)
                (INTEGERP N))
           (EQUAL (NEW-EXTERNAL-BOTTOM N (ADDITION-RING-CMPS S R)
                                       A)
                  (NEW-GROUP-OPERATION-BOTTOM N (NEW-EXTERNAL-BOTTOM N S A)
                                              (NEW-EXTERNAL-BOTTOM N R A))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING-CMPS S)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N (PRODUCT-RING-CMPS S R)
                                           A)
                      (NEW-EXTERNAL-BOTTOM N S (NEW-EXTERNAL-BOTTOM N R A))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N (UNIT-CMPS) A)
                      A))
      (IMPLIES
           (AND (NEW-INV-BOTTOM N A)
                (NEW-INV-BOTTOM N B)
                (INTEGERP N))
           (EQUAL (NEW-INVERSE-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B))
                  (NEW-GROUP-OPERATION-BOTTOM N (NEW-INVERSE-BOTTOM N A)
                                              (NEW-INVERSE-BOTTOM N B))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A)
                    (INV-RING-CMPS S)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-BOTTOM N (NEW-EXTERNAL-BOTTOM N S A))
                      (NEW-EXTERNAL-BOTTOM N S (NEW-INVERSE-BOTTOM N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (NEW-INVERSE-BOTTOM N (NEW-ZERO-BOTTOM N))
                      (NEW-ZERO-BOTTOM N)))
      (IMPLIES (AND (INV-RING-CMPS S) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-BOTTOM N S (NEW-ZERO-BOTTOM N))
                      (NEW-ZERO-BOTTOM N))))
     (AND
      (AND
          (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                   (NEW-INV-BOTTOM (+ N -1)
                                   (NEW-D-BOTTOM N A)))
          (IMPLIES (AND (NEW-INV-BOTTOM N A)
                        (NEW-INV-BOTTOM N B)
                        (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-GROUP-OPERATION-BOTTOM N A B))
                          (NEW-GROUP-OPERATION-BOTTOM (+ N -1)
                                                      (NEW-D-BOTTOM N A)
                                                      (NEW-D-BOTTOM N B))))
          (IMPLIES (AND (NEW-INV-BOTTOM N A)
                        (INV-RING-CMPS R)
                        (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-EXTERNAL-BOTTOM N R A))
                          (NEW-EXTERNAL-BOTTOM (+ N -1)
                                               R (NEW-D-BOTTOM N A))))
          (IMPLIES (INTEGERP N)
                   (EQUAL (NEW-D-BOTTOM N (NEW-ZERO-BOTTOM N))
                          (NEW-ZERO-BOTTOM (+ N -1))))
          (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                   (EQUAL (NEW-D-BOTTOM N (NEW-INVERSE-BOTTOM N A))
                          (NEW-INVERSE-BOTTOM (+ N -1)
                                              (NEW-D-BOTTOM N A)))))
      (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
               (EQUAL (NEW-D-BOTTOM (1- N) (NEW-D-BOTTOM N A))
                      (NEW-ZERO-BOTTOM (1- (1- N)))))))
    (AND
     (AND
      (AND
       (AND
           (AND (AND (IMPLIES (AND (INV-RING-CMPS X) (INV-RING-CMPS Y))
                              (INV-RING-CMPS (ADDITION-RING-CMPS X Y)))
                     (IMPLIES (AND (INV-RING-CMPS X)
                                   (INV-RING-CMPS Y)
                                   (INV-RING-CMPS Z))
                              (EQUAL (ADDITION-RING-CMPS (ADDITION-RING-CMPS X Y) Z)
                                     (ADDITION-RING-CMPS X (ADDITION-RING-CMPS Y Z)))))
                (IMPLIES (INV-RING-CMPS X)
                         (EQUAL (ADDITION-RING-CMPS (ZERO-ELEMENT-CMPS) X)
                                X))
                (IMPLIES (INV-RING-CMPS X)
                         (EQUAL (ADDITION-RING-CMPS X (ZERO-ELEMENT-CMPS))
                                X))
                (INV-RING-CMPS (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (EQUAL (ADDITION-RING-CMPS (INVERSE-CMPS X) X)
                           (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (EQUAL (ADDITION-RING-CMPS X (INVERSE-CMPS X))
                           (ZERO-ELEMENT-CMPS)))
           (IMPLIES (INV-RING-CMPS X)
                    (INV-RING-CMPS (INVERSE-CMPS X))))
       (AND (AND (IMPLIES (AND (INV-RING-CMPS X) (INV-RING-CMPS Y))
                          (INV-RING-CMPS (PRODUCT-RING-CMPS X Y)))
                 (IMPLIES (AND (INV-RING-CMPS X)
                               (INV-RING-CMPS Y)
                               (INV-RING-CMPS Z))
                          (EQUAL (PRODUCT-RING-CMPS (PRODUCT-RING-CMPS X Y) Z)
                                 (PRODUCT-RING-CMPS X (PRODUCT-RING-CMPS Y Z)))))
            (IMPLIES (INV-RING-CMPS X)
                     (EQUAL (PRODUCT-RING-CMPS (UNIT-CMPS) X) X))
            (IMPLIES (INV-RING-CMPS X)
                     (EQUAL (PRODUCT-RING-CMPS X (UNIT-CMPS)) X))
            (INV-RING-CMPS (UNIT-CMPS)))
       (IMPLIES (AND (INV-RING-CMPS X)
                     (INV-RING-CMPS Y)
                     (INV-RING-CMPS Z))
                (EQUAL (PRODUCT-RING-CMPS X (ADDITION-RING-CMPS Y Z))
                       (ADDITION-RING-CMPS (PRODUCT-RING-CMPS X Y)
                                      (PRODUCT-RING-CMPS X Z))))
       (IMPLIES (AND (INV-RING-CMPS X)
                     (INV-RING-CMPS Y)
                     (INV-RING-CMPS Z))
                (EQUAL (PRODUCT-RING-CMPS (ADDITION-RING-CMPS X Y) Z)
                       (ADDITION-RING-CMPS (PRODUCT-RING-CMPS X Z)
                                      (PRODUCT-RING-CMPS Y Z)))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (NEW-INV-TOP N (NEW-GROUP-OPERATION-TOP N A B)))
      (IMPLIES
       (AND (NEW-INV-TOP N A)
            (NEW-INV-TOP N B)
            (NEW-INV-TOP N C)
            (INTEGERP N))
       (EQUAL (NEW-GROUP-OPERATION-TOP N (NEW-GROUP-OPERATION-TOP N A B)
                                       C)
              (NEW-GROUP-OPERATION-TOP N A (NEW-GROUP-OPERATION-TOP N B C))))
      (NEW-INV-TOP N (NEW-ZERO-TOP N))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (NEW-INV-TOP N (NEW-EXTERNAL-TOP N R A)))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A (NEW-ZERO-TOP N))
                      A))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (NEW-INV-TOP N (NEW-INVERSE-TOP N A)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N)
                    (EQUAL (NEW-GROUP-OPERATION-TOP N A B)
                           (NEW-ZERO-TOP N)))
               (EQUAL (NEW-INVERSE-TOP N A) B))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A (NEW-INVERSE-TOP N A))
                      (NEW-ZERO-TOP N)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (EQUAL (NEW-GROUP-OPERATION-TOP N A B)
                      (NEW-GROUP-OPERATION-TOP N B A)))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N R (NEW-GROUP-OPERATION-TOP N A B))
                      (NEW-GROUP-OPERATION-TOP N (NEW-EXTERNAL-TOP N R A)
                                               (NEW-EXTERNAL-TOP N R B))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING-CMPS S)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (ADDITION-RING-CMPS S R)
                                        A)
                      (NEW-GROUP-OPERATION-TOP N (NEW-EXTERNAL-TOP N S A)
                                               (NEW-EXTERNAL-TOP N R A))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING-CMPS S)
                    (INV-RING-CMPS R)
                    (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (PRODUCT-RING-CMPS S R)
                                        A)
                      (NEW-EXTERNAL-TOP N S (NEW-EXTERNAL-TOP N R A))))
      (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N (UNIT-CMPS) A) A))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (NEW-INV-TOP N B)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-TOP N (NEW-GROUP-OPERATION-TOP N A B))
                      (NEW-GROUP-OPERATION-TOP N (NEW-INVERSE-TOP N A)
                                               (NEW-INVERSE-TOP N B))))
      (IMPLIES (AND (NEW-INV-TOP N A)
                    (INV-RING-CMPS S)
                    (INTEGERP N))
               (EQUAL (NEW-INVERSE-TOP N (NEW-EXTERNAL-TOP N S A))
                      (NEW-EXTERNAL-TOP N S (NEW-INVERSE-TOP N A))))
      (IMPLIES (INTEGERP N)
               (EQUAL (NEW-INVERSE-TOP N (NEW-ZERO-TOP N))
                      (NEW-ZERO-TOP N)))
      (IMPLIES (AND (INV-RING-CMPS S) (INTEGERP N))
               (EQUAL (NEW-EXTERNAL-TOP N S (NEW-ZERO-TOP N))
                      (NEW-ZERO-TOP N))))
     (AND (AND (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                        (NEW-INV-TOP (+ N -1) (NEW-D-TOP N A)))
               (IMPLIES (AND (NEW-INV-TOP N A)
                             (NEW-INV-TOP N B)
                             (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-GROUP-OPERATION-TOP N A B))
                               (NEW-GROUP-OPERATION-TOP (+ N -1)
                                                        (NEW-D-TOP N A)
                                                        (NEW-D-TOP N B))))
               (IMPLIES (AND (NEW-INV-TOP N A)
                             (INV-RING-CMPS R)
                             (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-EXTERNAL-TOP N R A))
                               (NEW-EXTERNAL-TOP (+ N -1)
                                                 R (NEW-D-TOP N A))))
               (IMPLIES (INTEGERP N)
                        (EQUAL (NEW-D-TOP N (NEW-ZERO-TOP N))
                               (NEW-ZERO-TOP (+ N -1))))
               (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                        (EQUAL (NEW-D-TOP N (NEW-INVERSE-TOP N A))
                               (NEW-INVERSE-TOP (+ N -1)
                                                (NEW-D-TOP N A)))))
          (IMPLIES (AND (NEW-INV-TOP N A) (INTEGERP N))
                   (EQUAL (NEW-D-TOP (1- N) (NEW-D-TOP N A))
                          (NEW-ZERO-TOP (1- (1- N)))))))
    (AND (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                  (NEW-INV-TOP N (NEW-G N A)))
         (IMPLIES (AND (NEW-INV-BOTTOM N A)
                       (NEW-INV-BOTTOM N B)
                       (INTEGERP N))
                  (EQUAL (NEW-G N (NEW-GROUP-OPERATION-BOTTOM N A B))
                         (NEW-GROUP-OPERATION-TOP N (NEW-G N A)
                                                  (NEW-G N B))))
         (IMPLIES (AND (NEW-INV-BOTTOM N A)
                       (INV-RING-CMPS R)
                       (INTEGERP N))
                  (EQUAL (NEW-G N (NEW-EXTERNAL-BOTTOM N R A))
                         (NEW-EXTERNAL-TOP N R (NEW-G N A))))
         (IMPLIES (INTEGERP N)
                  (EQUAL (NEW-G N (NEW-ZERO-BOTTOM N))
                         (NEW-ZERO-TOP N)))
         (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
                  (EQUAL (NEW-G N (NEW-INVERSE-BOTTOM N A))
                         (NEW-INVERSE-TOP N (NEW-G N A)))))
    (IMPLIES (AND (NEW-INV-BOTTOM N A) (INTEGERP N))
             (EQUAL (NEW-D-TOP N (NEW-G N A))
                    (NEW-G (1- N) (NEW-D-BOTTOM N A)))))
   (IMPLIES (AND (NEW-INV-BOTTOM N GNRT)
                 (INTEGERP N))
            (EQUAL (NEW-F N (NEW-G N GNRT)) GNRT))
   (IMPLIES
    (AND (NEW-INV-TOP N GNRT) (INTEGERP N))
    (EQUAL
     (NEW-GROUP-OPERATION-TOP N (NEW-H (1- N) (NEW-D-TOP N GNRT))
                              (NEW-D-TOP (1+ N) (NEW-H N GNRT)))
     (NEW-GROUP-OPERATION-TOP N GNRT
                              (NEW-INVERSE-TOP N (NEW-G N (NEW-F N GNRT))))))
   (IMPLIES (AND (NEW-INV-TOP N GNRT) (INTEGERP N))
            (EQUAL (NEW-F (1+ N) (NEW-H N GNRT))
                   (NEW-ZERO-BOTTOM (1+ N))))
   (IMPLIES (AND (NEW-INV-BOTTOM N GNRT)
                 (INTEGERP N))
            (EQUAL (NEW-H N (NEW-G N GNRT))
                   (NEW-ZERO-TOP (1+ N))))
   (IMPLIES (AND (NEW-INV-TOP N GNRT) (INTEGERP N))
            (EQUAL (NEW-H (1+ N) (NEW-H N GNRT))
                   (NEW-ZERO-TOP (1+ (1+ N))))))
  :HINTS (("Subgoal 51" :USE ((:INSTANCE TOP-AUX-PROP2)))
          ("Subgoal 35" :USE ((:INSTANCE BOTTOM-AUX-PROP2)))
          ("Subgoal 15" :USE ((:INSTANCE NEW-DISTRIBUTIVITY-H)))
          ("Subgoal 4" :USE ((:INSTANCE NEW-HOD+DOH (A GNRT)))))))
  )


(make-generic-theory *cmps*)